docs: TLA+ full-verification run guide#14
Merged
Conversation
Adds tla/RUN_FULL_VERIFICATION.md, a self-contained run book that takes a
fresh runner from "I have the repo and Java" to "all configs verified".
Covers:
- Which specs / configs to run, in cheapest-first order (Minimal smoke ->
Medium -> Standard ~5h -> Stress optional)
- Exact TLC invocation (must run from tla/ directory; -Xmx tuning;
nohup / tmux pattern for the long ones)
- Resource estimates (Standard needs ~60 GB RAM; Stress can OOM)
- The KernelCcCache sanity pair (must-pass and must-fail-deterministically)
- What to report back; what NOT to do (don't shrink configs to make them
pass, don't disable invariants, don't run Standard and Stress in parallel)
CI only runs Minimal (~12 min). The larger configs need a dedicated machine,
so this guide lives next to the specs and tells whoever runs them what's
expected.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hooyao
force-pushed
the
docs-tla-full-verification-guide
branch
from
b76caa8 to
8a52525
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
tla/RUN_FULL_VERIFICATION.md— a self-contained run book for executing the full TLA+ suite on a high-RAM workstation.CI only runs
RamDiskSystem_Minimal.cfg(~12 min). The larger configs (Medium, Standard, Stress) need 10–60 GB RAM and many hours of wall-clock time, so they don't belong on CI but the runner instructions should still live in the repo.The guide covers:
tla/directory;-Xmxtuning;nohup/tmuxpattern for the multi-hour runs)KernelCcCachesanity pair (must-pass + must-fail-deterministically)Test plan
🤖 Generated with Claude Code